Nuprl Definition : nat-deq
0,22
postcript
pdf
NatDeq == <
a
,
b
.
a
=
b
,TERMOF{
nat-deq-aux
:ObjectId, 1:l}>
latex
Definitions
nat-deq-aux
,
i
=
j
FDL editor aliases
nat-deq
origin
a,b. a=
b,TERMOF{nat-deq-aux:ObjectId, 1:l}> a,b. a=b,TERMOF{nat-deq-aux:ObjectId, 1:l}> j